﻿using System;
using System.Collections.Generic;
using System.IO;
using System.Linq;
using TSU.FAMC.ComputerEngineering.Classes.Bdds;
using TSU.FAMC.ComputerEngineering.Classes.BooleanMaths.Functions;
using TSU.FAMC.ComputerEngineering.Classes.Enums;
using TSU.FAMC.ComputerEngineering.Classes.BooleanMaths.Fundamental;
using TSU.FAMC.ComputerEngineering.Classes.OrandTrees;
using TSU.FAMC.ComputerEngineering.Classes.OrandTrees.Basis;
using TSU.FAMC.ComputerEngineering.Classes.OrandTrees.Readers;
using TSU.FAMC.ComputerEngineering.Classes.Circuits;
using TSU.FAMC.ComputerEngineering.Classes.Circuits.Basis;
using System.Collections;

namespace TSU.FAMC.ComputerEngineering.Classes.Diagnostics.PathDelayFaults
{
    /// <summary>
    /// Analyzes arbitrary circuit against path delay faults (robust and non-robust).
    /// </summary>
    public static class PathDelayFaultAnalyzer
    {
        /// <summary>
        /// Builds test for path-delay faults (robust and non-robust) for circuit.
        /// </summary>
        /// <param name="circuit">Circuit to build test for.</param>
        /// <returns>List of pdf tests.</returns>
        public static List<PdfTest> BuildTest(Circuit circuit)
        {
            // checking whether circuit has back links (flip flops)
            if (circuit.Elements.Any(e => e is FlipFlop))
            {
                // extracting combinational equivalent to analyze
                circuit = circuit.ExtractCombinationalEquivalent();
            }

            var test = new List<PdfTest>();

            // reading tree
            var treeReader = new OrandTreeReaderCircuit { Input = circuit };
            treeReader.Read();

            // calculating cubes dimension
            var inputMarks = treeReader.Tree.GetInputsOrder();
            var dimension = inputMarks.Count;

            foreach (var top in treeReader.Tree.Tops)
            {
                // extracting corresponding subtree
                var tree = treeReader.Tree.ExtractTree(top);

                // iterating leaves of OR,AND-tree (paths iteration)
                foreach (var leaf in tree.Leaves)
                {
                    var inputIndex = inputMarks.IndexOf(OrandTree.GetInputMark(leaf));

                    // retrieving path sub-tree
                    var pathTree = tree.PathSensitization(leaf);

                    // retrieving tree without path sub-tree
                    var decisionTree = tree.ExcludePath(leaf);

                    // retrieving conjunctions containing path
                    var pathConjunctions = (from object conj in pathTree select conj as ElementInterface).ToList();

                    // preparing list object for originative conjunctions
                    var originativeConjunctions = new List<ElementInterface>();

                    // preparing list for equation roots
                    var equationRoots = new List<ElementInterface>();



                    // 1. Trying build robust test for path.
                    var robustTestFound = false;

                    // excluding some conjunctions from path conjunctions list
                    foreach (var pathConjunction in pathConjunctions)
                    {
                        // TODO: test it
                        var inputValues = new List<KeyValuePair<string, bool>>();
                        var isExcluded = false;
                        foreach (Vertex conjunctionLeaf in pathConjunction)
                        {
                            if (
                                inputValues.Any(p => p.Key == conjunctionLeaf.Data.ToString() && p.Value == !conjunctionLeaf.IsInverted))
                            {
                                // excluding empty conjunctions
                                isExcluded = true;
                                break;
                            }

                            if (inputValues.Any(p => p.Key == conjunctionLeaf.Data.ToString()) &&
                                inputMarks.IndexOf(conjunctionLeaf.Data.ToString()) == inputIndex)
                            {
                                // excluding conjunctions with repeating path-variable
                                isExcluded = true;
                                break;
                            }

                            if (
                                inputValues.Any(p => p.Key == conjunctionLeaf.Data.ToString() && p.Value == conjunctionLeaf.IsInverted))
                            {
                                // skipping repeating non-path variables
                                continue;
                            }

                            inputValues.Add(new KeyValuePair<string, bool>(conjunctionLeaf.Data.ToString(), conjunctionLeaf.IsInverted));
                        }

                        if (!isExcluded)
                        {
                            originativeConjunctions.Add(pathConjunction);
                        }
                    }


                    // iterativng originative conjunctions to find test
                    foreach (var originativeConjunction in originativeConjunctions)
                    {
                        // building cube for conjunction
                        var cube = BuildCubeFromConjunction(originativeConjunction, dimension, inputMarks);
                        if (originativeConjunction.Count == 0 || cube == null || cube.Rank == 0)
                        {
                            // invalid conjunction
                            throw new Exception("Invalid conjunction!");
                        }


                        // fixing variables of decision tree except path variable
                        var fixingCube = new Cube(cube);
                        fixingCube[inputIndex] = BooleanValue.Undefined;
                        var decisionTreeFixed = (OrandTree)decisionTree.Clone(); // TODO: bottleneck
                        decisionTreeFixed.InputsOrder = inputMarks; // preserving inputs order
                        decisionTreeFixed.FixInputs(fixingCube);

                        if (decisionTreeFixed.Tops[0].Type == VertexType.Constant0)
                        {
                            // D == 0

                            // building test vectors
                            var testPrototype = new Cube(fixingCube);

                            var v1 = new Cube(testPrototype);
                            v1[inputIndex] = leaf.IsInverted ? BooleanValue.True : BooleanValue.False;
                            var v2 = new Cube(testPrototype);
                            v2[inputIndex] = leaf.IsInverted ? BooleanValue.False : BooleanValue.True;

                            var robustTest = new PdfTest
                                                 {
                                                     V1 = v1,
                                                     V2 = v2,
                                                     Path = tree.GetPathList(leaf),
                                                     FaultType = PdfType.Robust,
                                                     FunctionIndex = treeReader.Tree.Tops.IndexOf(top)
                                                 };
                            test.Add(robustTest);
                        }
                        else if (decisionTreeFixed.Tops[0].Type == VertexType.Constant1)
                        {
                            // D == 1, no roots for current conjunction
                            continue;
                        }
                        else
                        {
                            // Searching for root

                            // inverting decision tree to solve equation !D=1 (D=0)
                            decisionTreeFixed.Invert();


                            // retrieving first valid equation root
                            var rootFound = false;
                            var firstValidRoot = new Cube();
                            foreach (ElementInterface conjunction in decisionTreeFixed)
                            {
                                // filtering roots with path variable
                                if (conjunction.Any(te => te.Data != null && inputMarks.IndexOf(te.Data.ToString()) == inputIndex))
                                {
                                    continue;
                                }

                                // trying build cube
                                var rootCube = BuildCubeFromConjunction(conjunction, dimension, inputMarks);
                                if (rootCube == null || rootCube.Dimension == 0)
                                {
                                    // incompatible conjunction
                                    continue;
                                }

                                // valid root found
                                firstValidRoot = rootCube;
                                rootFound = true;
                                break;
                            }

                            if (!rootFound)
                            {
                                // no roots
                                continue;
                            }

                            /*
                            equationRoots.Clear();
                            var conjunctionsCount = decisionTreeFixed.CountConjunctions();
                            equationRoots.AddRange(decisionTreeFixed.Cast<ElementInterface>());

                            // filtering roots with path variable
                            equationRoots =
                                equationRoots.Where(
                                    e => !e.Any(te => te.Data != null && inputMarks.IndexOf(te.Data.ToString()) == inputIndex)).
                                    ToList();

                            if (equationRoots.Count == 0)
                            {
                                // no roots
                                continue;
                            }

                            // searching for first consistent root
                            var firstValidRoot = new Cube();
                            foreach (var equationRoot in equationRoots)
                            {
                                var rootCube = BuildCubeFromConjunction(equationRoot, dimension, inputMarks);
                                if (rootCube == null)
                                {
                                    continue;
                                }

                                firstValidRoot = rootCube;
                                break;
                            }


                            if (firstValidRoot.Dimension == 0)
                            {
                                // no valid root
                                continue;
                            }
                             */

                            // building test vectors
                            var testPrototype = new Cube(firstValidRoot);
                            for (var i = 0; i < dimension; i++)
                            {
                                if (fixingCube[i] == BooleanValue.Undefined)
                                {
                                    continue;
                                }
                                testPrototype[i] = fixingCube[i];
                            }

                            var v1 = new Cube(testPrototype);
                            v1[inputIndex] = leaf.IsInverted ? BooleanValue.True : BooleanValue.False;
                            var v2 = new Cube(testPrototype);
                            v2[inputIndex] = leaf.IsInverted ? BooleanValue.False : BooleanValue.True;

                            var robustTest = new PdfTest
                                                 {
                                                     V1 = v1,
                                                     V2 = v2,
                                                     Path = tree.GetPathList(leaf),
                                                     FaultType = PdfType.Robust,
                                                     FunctionIndex = treeReader.Tree.Tops.IndexOf(top)
                                                 };
                            test.Add(robustTest);
                        }


                        robustTestFound = true;
                        break;
                    }


                    if (robustTestFound)
                    {
                        // next path
                        continue;
                    }


                    // 2. Trying build non-robust test for path.
                    pathConjunctions = (from object conj in pathTree select conj as ElementInterface).ToList();

                    // 2.1 Non-robust B-fault.
                    var nonrobustTestFound = false;

                    // excluding some conjunctions from path conjunctions list
                    originativeConjunctions.Clear();
                    foreach (var pathConjunction in pathConjunctions)
                    {
                        var inputValues = new List<KeyValuePair<string, bool>>();
                        var isExcluded = false;
                        foreach (Vertex conjunctionLeaf in pathConjunction)
                        {
                            if (inputValues.Any(p => p.Key == conjunctionLeaf.Data.ToString() && p.Value == !conjunctionLeaf.IsInverted)
                                && inputMarks.IndexOf(conjunctionLeaf.Data.ToString()) != inputIndex)
                            {
                                // excluding empty via non path-variable conjunctions
                                isExcluded = true;
                                break;
                            }

                            if (inputValues.Any(p => p.Key == conjunctionLeaf.Data.ToString())
                                && inputMarks.IndexOf(conjunctionLeaf.Data.ToString()) == inputIndex)
                            {
                                // excluding conjunctions with repeating path-variable
                                isExcluded = true;
                                break;
                            }

                            if (
                                inputValues.Any(p => p.Key == conjunctionLeaf.Data.ToString() && p.Value == conjunctionLeaf.IsInverted))
                            {
                                // skipping repeating non-path variables
                                continue;
                            }

                            inputValues.Add(new KeyValuePair<string, bool>(conjunctionLeaf.Data.ToString(), conjunctionLeaf.IsInverted));
                        }

                        if (!isExcluded)
                        {
                            // inverting path variable
                            var pathVar = pathConjunction.SingleOrDefault(te => pathTree.GetPath((Vertex)te.RelatedElement) == tree.GetPath(leaf));
                            if (pathVar == null)
                            {
                                throw new Exception("Could not find path variable!");
                            }

                            var pathVertex = (Vertex) pathVar;
                            pathVertex.IsInverted = !pathVertex.IsInverted;

                            originativeConjunctions.Add(pathConjunction);
                        }
                    }


                    // iterativng originative conjunctions to find test
                    foreach (var originativeConjunction in originativeConjunctions)
                    {
                        // building cube for conjunction
                        var cube = BuildCubeFromConjunction(originativeConjunction, dimension, inputMarks);
                        if (originativeConjunction.Count == 0 || cube == null || cube.Rank == 0)
                        {
                            // invalid conjunction
                            throw new Exception("Empty or invalid conjunction! Something wrong.");
                        }


                        // fixing variables of decision tree (with inverted path variable)!
                        var fixingCube = new Cube(cube);

                        // retrieving decision tree
                        var decisionTreeFixed = (OrandTree)tree.Clone(); // decision tree as hole tree!
                        

                        decisionTreeFixed.InputsOrder = inputMarks; // preserving inputs order
                        decisionTreeFixed.FixInputs(fixingCube);

                        if (decisionTreeFixed.Tops[0].Type == VertexType.Constant0)
                        {
                            // D == 0

                            // building test vectors
                            var testPrototype = new Cube(fixingCube);

                            var v1 = new Cube(testPrototype);
                            v1[inputIndex] = leaf.IsInverted ? BooleanValue.True : BooleanValue.False;
                            var v2 = new Cube(testPrototype);
                            v2[inputIndex] = leaf.IsInverted ? BooleanValue.False : BooleanValue.True;

                            var nonrobustTest = new PdfTest
                                                 {
                                                     V1 = v1,
                                                     V2 = v2,
                                                     Path = tree.GetPathList(leaf),
                                                     FaultType = PdfType.Nonrobust,
                                                     SopFaultType = SopFaultType.B,
                                                     FunctionIndex = treeReader.Tree.Tops.IndexOf(top)
                                                 };
                            test.Add(nonrobustTest);
                        }
                        else if (decisionTreeFixed.Tops[0].Type == VertexType.Constant1)
                        {
                            // D == 1, no roots for current conjunction
                            continue;
                        }
                        else
                        {
                            // Searching for root

                            // inverting decision tree to solve equation !D=1 (D=0)
                            decisionTreeFixed.Invert();


                            // retrieving equation roots
                            equationRoots.Clear();
                            equationRoots.AddRange(decisionTreeFixed.Cast<ElementInterface>());

                            if (equationRoots.Count == 0)
                            {
                                // no roots
                                continue;
                            }

                            // searching for first consistent root
                            var firstValidRoot = new Cube();
                            foreach (var equationRoot in equationRoots)
                            {
                                var rootCube = BuildCubeFromConjunction(equationRoot, dimension, inputMarks);
                                if (rootCube == null)
                                {
                                    continue;
                                }

                                firstValidRoot = rootCube;
                                break;
                            }


                            if (firstValidRoot.Dimension == 0)
                            {
                                // no valid root
                                continue;
                            }

                            // building test vectors
                            var testPrototype = new Cube(firstValidRoot);
                            for (var i = 0; i < dimension; i++)
                            {
                                if (fixingCube[i] == BooleanValue.Undefined)
                                {
                                    continue;
                                }
                                testPrototype[i] = fixingCube[i];
                            }

                            var v1 = new Cube(testPrototype);
                            v1[inputIndex] = leaf.IsInverted ? BooleanValue.True : BooleanValue.False;
                            var v2 = new Cube(testPrototype);
                            v2[inputIndex] = leaf.IsInverted ? BooleanValue.False : BooleanValue.True;

                            var nonrobustTest = new PdfTest
                                                 {
                                                     V1 = v1,
                                                     V2 = v2,
                                                     Path = tree.GetPathList(leaf),
                                                     FaultType = PdfType.Nonrobust,
                                                     SopFaultType = SopFaultType.B,
                                                     FunctionIndex = treeReader.Tree.Tops.IndexOf(top)
                                                 };
                            test.Add(nonrobustTest);
                        }


                        nonrobustTestFound = true;
                        break;
                    }


                    // 2.2 Non-robust A-fault.
                    pathConjunctions = (from object conj in pathTree select conj as ElementInterface).ToList();

                    // excluding some conjunctions from path conjunctions list
                    originativeConjunctions.Clear();
                    foreach (var pathConjunction in pathConjunctions)
                    {
                        var inputValues = new List<KeyValuePair<string, bool>>();
                        var isExcluded = false;
                        foreach (Vertex conjunctionLeaf in pathConjunction)
                        {
                            if (
                                inputValues.Any(p => p.Key == conjunctionLeaf.Data.ToString() && p.Value == !conjunctionLeaf.IsInverted))
                            {
                                // excluding all empty conjunctions
                                isExcluded = true;
                                break;
                            }

                            // leaving conjunctions with repeating variables

                            inputValues.Add(new KeyValuePair<string, bool>(conjunctionLeaf.Data.ToString(), conjunctionLeaf.IsInverted));
                        }

                        if (!isExcluded)
                        {
                            originativeConjunctions.Add(pathConjunction);
                        }
                    }


                    // iterativng originative conjunctions to find test
                    foreach (var originativeConjunction in originativeConjunctions)
                    {
                        // building cube for conjunction
                        var cube = BuildCubeFromConjunction(originativeConjunction, dimension, inputMarks);
                        if (originativeConjunction.Count == 0 || cube == null || cube.Rank == 0)
                        {
                            // invalid conjunction
                            throw new Exception("Invalid conjunction!");
                        }


                        // fixing variables of decision tree and inverting path variable!
                        var fixingCube = new Cube(cube); // path variables included
                        var decisionTreeFixed = (OrandTree) decisionTree.Clone();
                        decisionTreeFixed.InputsOrder = inputMarks; // preserving inputs order
                        decisionTreeFixed.FixInputs(fixingCube);

                        if (decisionTreeFixed.Tops[0].Type == VertexType.Constant0)
                        {
                            // D == 0

                            // building test vectors
                            var testPrototype = new Cube(fixingCube);

                            var v1 = new Cube(testPrototype);
                            v1[inputIndex] = leaf.IsInverted ? BooleanValue.False : BooleanValue.True;
                            var v2 = new Cube(testPrototype);
                            v2[inputIndex] = leaf.IsInverted ? BooleanValue.True : BooleanValue.False;

                            var nonrobustTest = new PdfTest
                                                 {
                                                     V1 = v1,
                                                     V2 = v2,
                                                     Path = tree.GetPathList(leaf),
                                                     FaultType = PdfType.Nonrobust,
                                                     SopFaultType = SopFaultType.A,
                                                     FunctionIndex = treeReader.Tree.Tops.IndexOf(top)
                                                 };
                            test.Add(nonrobustTest);
                        }
                        else if (decisionTreeFixed.Tops[0].Type == VertexType.Constant1)
                        {
                            // D == 1, no roots for current conjunction
                            continue;
                        }
                        else
                        {
                            // Searching for root

                            // inverting decision tree to solve equation !D=1 (D=0)
                            decisionTreeFixed.Invert();


                            // retrieving equation roots
                            equationRoots.Clear();
                            equationRoots.AddRange(decisionTreeFixed.Cast<ElementInterface>());

                            if (equationRoots.Count == 0)
                            {
                                // no roots
                                continue;
                            }

                            // searching for first consistent root
                            var firstValidRoot = new Cube();
                            foreach (var equationRoot in equationRoots)
                            {
                                var rootCube = BuildCubeFromConjunction(equationRoot, dimension, inputMarks);
                                if (rootCube == null)
                                {
                                    continue;
                                }

                                firstValidRoot = rootCube;
                                break;
                            }


                            if (firstValidRoot.Dimension == 0)
                            {
                                // no valid root
                                continue;
                            }

                            // building test vectors
                            var testPrototype = new Cube(firstValidRoot);
                            for (var i = 0; i < dimension; i++)
                            {
                                if (fixingCube[i] == BooleanValue.Undefined)
                                {
                                    continue;
                                }
                                testPrototype[i] = fixingCube[i];
                            }

                            var v1 = new Cube(testPrototype);
                            v1[inputIndex] = leaf.IsInverted ? BooleanValue.False : BooleanValue.True;
                            var v2 = new Cube(testPrototype);
                            v2[inputIndex] = leaf.IsInverted ? BooleanValue.True : BooleanValue.False;

                            var nonrobustTest = new PdfTest
                                                 {
                                                     V1 = v1,
                                                     V2 = v2,
                                                     Path = tree.GetPathList(leaf),
                                                     FaultType = PdfType.Nonrobust,
                                                     SopFaultType = SopFaultType.A,
                                                     FunctionIndex = treeReader.Tree.Tops.IndexOf(top)
                                                 };
                            test.Add(nonrobustTest);
                        }


                        nonrobustTestFound = true;
                        break;
                    }


                    if (nonrobustTestFound)
                    {
                        // next path
                        continue;
                    }



                    // 3. False path detected.

                    var falseTest = new PdfTest
                    {
                        Path = tree.GetPathList(leaf),
                        FaultType = PdfType.False,
                        FunctionIndex = treeReader.Tree.Tops.IndexOf(top)
                    };

                    test.Add(falseTest);
                }

            }

            return test;
        }

        /// <summary>
        /// Builds cube of minimum dimension for conjunction leaves.
        /// </summary>
        /// <param name="conjunction">List of leaf vertices of OrandTree object.</param>
        /// <param name="dim">Required cube dimension.</param>
        /// <param name="inputsOrder">List of input marks to determing inputs order.</param>
        /// <returns>Cube representation of the conjunction.</returns>
        private static Cube BuildCubeFromConjunction(List<TreeElement> conjunction, int dim, IList<string> inputsOrder)
        {
            if (conjunction == null)
            {
                throw new ArgumentNullException("conjunction");
            }

            var dimension = 0;
            if (dim > 0)
            {
                dimension = dim;
            }
            else
            {
                // determing minimum dimension
                foreach (Vertex leaf in conjunction)
                {
                    if (leaf.Type == VertexType.Constant0 ||
                        leaf.Type == VertexType.Constant1)
                    {
                        continue;
                    }

                    var inputMark = OrandTree.GetInputMark(leaf);
                    var inputNumber = inputsOrder.IndexOf(inputMark);

                    if (inputNumber > dimension)
                    {
                        dimension = inputNumber;
                    }
                }

                dimension++;
            }

            // building cube
            var cube = new Cube(dimension);
            cube.Init(BooleanValue.Undefined);

            foreach (Vertex vertex in conjunction)
            {
                if ((vertex.Type == VertexType.Constant1 && !vertex.IsInverted) ||
                    (vertex.Type == VertexType.Constant0 && vertex.IsInverted))
                {
                    // constant 1
                    return null;
                }

                if ((vertex.Type == VertexType.Constant1 && vertex.IsInverted) ||
                    (vertex.Type == VertexType.Constant0 && !vertex.IsInverted))
                {
                    // constant 0
                    return null;
                }

                if (vertex.Type != VertexType.Input ||
                    vertex.Data as String == "")
                {
                    throw new InvalidDataException("Leaf vertex of ORAND-tree must have input number in the Data property and have a Type == VertexType.UNDEFINED");
                }

                var inputNumberStr = vertex.Data.ToString();
                var inputNumber = inputsOrder.IndexOf(inputNumberStr);

                if (cube[inputNumber] != BooleanValue.Undefined &&
                    cube[inputNumber] != (vertex.IsInverted ? BooleanValue.False : BooleanValue.True))
                {
                    // empty conjunction (x*!x)
                    return null;
                }

                cube[inputNumber] = vertex.IsInverted ? BooleanValue.False : BooleanValue.True;
            }

            return cube;
        }

        /// <summary>
        /// Calculates probabilities of manifestation of robust Pdfs for state variables.
        /// </summary>
        /// <param name="circuit">Circuit to analyze.</param>
        /// <param name="inputProabilities">Probabilities of 1-input signal (for inputs and state variables).</param>
        /// <returns>List of pdf tests.</returns>
        public static List<List<FlipFlopStats>> CalculateRobustObservabilities(Circuit circuit, Dictionary<string, double> inputProabilities = null)
        {
            // checking whether circuit has back links (flip flops)
            if (!circuit.Elements.Any(e => e is FlipFlop))
            {
                throw new Exception("Specified circuit does not contain any state variables!");
            }

            // retrieving input marks corresponding to state variables (flip flops)
            var stateVariableMarks = circuit.Elements.Where(e => e is FlipFlop).Select(e => e.Name).ToList();

            // extracting combinational equivalent to analyze
            circuit = circuit.ExtractCombinationalEquivalent();

            var result = new List<List<FlipFlopStats>>();

            // reading tree
            var treeReader = new OrandTreeReaderCircuit { Input = circuit };
            treeReader.Read();

            // calculating cubes dimension
            var inputMarks = treeReader.Tree.GetInputsOrder();
            if (inputProabilities == null || inputProabilities.Count == 0)
            {
                // init input probabilities with 0.5
                inputProabilities = inputMarks.ToDictionary(inputMark => inputMark, inputMark => 0.5);
            }

            if (inputMarks.Count != inputProabilities.Count)
            {
                throw new Exception("Probabilities for all inputs should be specified (including state variables)");
            }

            var stateVariablesOrderedIndices = stateVariableMarks.Select(st => inputMarks.IndexOf(st)).OrderBy(i => i).ToList();

            // calculating probabilities for each flip flop
            var dimension = inputMarks.Count;
            foreach (var stateVariableMark in stateVariableMarks)
            {
                // calculating indices
                var currentStateVarIndex = inputMarks.IndexOf(stateVariableMark);
                var previousToCurrentStateVarIndex = stateVariablesOrderedIndices[0] == currentStateVarIndex
                                                         ? stateVariablesOrderedIndices[
                                                             stateVariablesOrderedIndices.Count - 1]
                                                         : stateVariablesOrderedIndices[
                                                             stateVariablesOrderedIndices.IndexOf(currentStateVarIndex) -
                                                             1];
                var nextToCurrentStateVarIndex = stateVariablesOrderedIndices[stateVariablesOrderedIndices.Count - 1] ==
                                                 currentStateVarIndex
                                                     ? stateVariablesOrderedIndices[0]
                                                     : stateVariablesOrderedIndices[
                                                         stateVariablesOrderedIndices.IndexOf(currentStateVarIndex) +
                                                         1];

                var circuitTree = treeReader.Tree;

                // iterating tree tops (circuit outputs)
                var resultsFroDifferentTreeTops = new List<FlipFlopStats>();
                var outputMarks = new List<string>();
                foreach (var top in circuitTree.Tops)
                {
                    var outputMark = top.Data.ToString();
                    if (outputMark.Contains(","))
                    {
                        outputMark = outputMark.Substring(0, outputMark.IndexOf(",", StringComparison.Ordinal));
                    }
                    outputMarks.Add(outputMark);

                    // searching for tree top corresponding to variable
                    /*
                    var tops =
                        treeReader.Tree.Tops.Where(
                            t =>
                            t.Children.Count > 0 &&
                            (t.Data.ToString() == stateVariableMark ||
                            t.Data.ToString().StartsWith(stateVariableMark + ","))).ToList();
                    if (tops.Count > 1)
                    {
                        throw new Exception("Could not find unique tree top corresponding to flip flop!");
                    }
                    var top = tops.First();
                    if (top == null)
                    {
                        throw new Exception("Could not find tree top corresponding to state variable");
                    }
                    */

                    // extracting corresponding subtree
                    var tree = circuitTree.ExtractTree(top);

                    // searching for leaves corresponding to state variable
                    var leaves = tree.Leaves.Where(l => OrandTree.GetInputMark(l) == stateVariableMark).ToList();

                    // iterating leaves corresponding to current state variable and different paths
                    var observability = 0.0;
                    var losObservability = 0.0;

                    var robustSensitezationConditions = new List<Hashtable>();

                    #region State var leaves iteration
                    foreach (var leaf in leaves)
                    {
                        var robustSensitezationConditionsForCurrentPath = new Hashtable();

                        var inputIndex = inputMarks.IndexOf(OrandTree.GetInputMark(leaf));

                        // retrieving path sub-tree
                        var pathTree = tree.PathSensitization(leaf);

                        // retrieving tree without path sub-tree
                        var decisionTree = tree.ExcludePath(leaf);

                        // retrieving conjunctions containing path
                        var pathConjunctions = (from object conj in pathTree select conj as ElementInterface).ToList();

                        // preparing list object for originative conjunctions
                        var originativeConjunctionLeaves = new List<ElementInterface>();

                        // preparing list for equation roots
                        var equationRoots = new List<ElementInterface>();


                        // Trying build robust test for path.

                        // excluding some conjunctions from path conjunctions list
                        foreach (var pathConjunction in pathConjunctions)
                        {
                            var inputValues = new List<KeyValuePair<string, bool>>();
                            var isExcluded = false;
                            foreach (Vertex conjunctionLeaf in pathConjunction)
                            {
                                if (
                                    inputValues.Any(
                                        p =>
                                        p.Key == conjunctionLeaf.Data.ToString() &&
                                        p.Value == !conjunctionLeaf.IsInverted))
                                {
                                    // excluding empty conjunctions
                                    isExcluded = true;
                                    break;
                                }

                                if (inputValues.Any(p => p.Key == conjunctionLeaf.Data.ToString()) &&
                                    inputMarks.IndexOf(conjunctionLeaf.Data.ToString()) == inputIndex)
                                {
                                    // excluding conjunctions with repeating path-variable
                                    isExcluded = true;
                                    break;
                                }

                                if (
                                    inputValues.Any(
                                        p =>
                                        p.Key == conjunctionLeaf.Data.ToString() &&
                                        p.Value == conjunctionLeaf.IsInverted))
                                {
                                    // skipping repeating non-path variables
                                    continue;
                                }

                                inputValues.Add(new KeyValuePair<string, bool>(conjunctionLeaf.Data.ToString(),
                                                                               conjunctionLeaf.IsInverted));
                            }

                            if (!isExcluded)
                            {
                                originativeConjunctionLeaves.Add(pathConjunction);
                            }
                        }

                        // building cubes from tree leaves and excluding duplicats
                        var originativeConjunctions = new HashSet<Cube>();
                        foreach (var originativeConjunctionLeaf in originativeConjunctionLeaves)
                        {
                            // building cube for conjunction
                            var cube = BuildCubeFromConjunction(originativeConjunctionLeaf, dimension, inputMarks);
                            if (originativeConjunctionLeaf.Count == 0 || cube == null || cube.Rank == 0)
                            {
                                // invalid conjunction
                                throw new Exception("Invalid conjunction!");
                            }

                            if (!originativeConjunctions.Contains(cube))
                            {
                                originativeConjunctions.Add(cube);
                            }
                        }

                        // iterativng originative conjunctions to find robust conditions
                        OrderedBdd rootsBdd = null;
                        foreach (var cube in originativeConjunctions)
                        {
                            OrderedBdd rootsForOriginativeConjunctionBdd = null;
                            var robustSensitezationConditionsForCurrentConjunction = new List<Cube>();

                            // fixing variables of decision tree except path variable
                            var fixingCube = new Cube(cube);
                            fixingCube[inputIndex] = BooleanValue.Undefined; // reseting state variable
                            var decisionTreeFixed = (OrandTree) decisionTree.Clone();
                            decisionTreeFixed.InputsOrder = inputMarks; // preserving inputs order
                            decisionTreeFixed.FixInputs(fixingCube);

                            if (decisionTreeFixed.Tops[0].Type == VertexType.Constant0)
                            {
                                // D == 0, always robust pdf manifestation for current conjunction
                                var testPrototype = new Cube(fixingCube);

                                // memorizing robust PDF manifestation condition
                                robustSensitezationConditionsForCurrentConjunction.Add(testPrototype);

                                var rootBdd = OrderedBdd.BuildFromCube(testPrototype, inputMarks);
                                rootsForOriginativeConjunctionBdd = rootBdd;
                            }
                            else if (decisionTreeFixed.Tops[0].Type == VertexType.Constant1)
                            {
                                // D == 1, always not a robust manifistation for current conjunction
                                // going to the next conjunction
                                continue;
                            }
                            else
                            {
                                // Searching for root

                                // inverting decision tree to solve equation !D=1 (D=0)
                                decisionTreeFixed.Invert();

                                equationRoots.Clear();
                                equationRoots.AddRange(decisionTreeFixed.Cast<ElementInterface>());

                                // filtering roots with path variable
                                equationRoots =
                                    equationRoots.Where(
                                        e =>
                                        !e.Any(
                                            te =>
                                            te.Data != null && inputMarks.IndexOf(te.Data.ToString()) == inputIndex)).
                                        ToList();

                                if (equationRoots.Count == 0)
                                {
                                    // no roots
                                    continue;
                                }

                                // searching for first consistent root
                                foreach (var equationRoot in equationRoots)
                                {
                                    var rootCube = BuildCubeFromConjunction(equationRoot, dimension, inputMarks);
                                    if (rootCube == null)
                                    {
                                        continue;
                                    }

                                    // valid root found

                                    // building test prototype
                                    var testPrototype = new Cube(rootCube);
                                    for (var i = 0; i < dimension; i++)
                                    {
                                        if (fixingCube[i] == BooleanValue.Undefined)
                                        {
                                            continue;
                                        }
                                        testPrototype[i] = fixingCube[i];
                                    }

                                    // building bdd representing root
                                    var rootBdd = OrderedBdd.BuildFromCube(testPrototype, inputMarks);

                                    // memorizing robust PDF manifestation condition
                                    robustSensitezationConditionsForCurrentConjunction.Add(testPrototype);

                                    // appending condition
                                    rootsForOriginativeConjunctionBdd = rootsForOriginativeConjunctionBdd == null ? rootBdd : rootsForOriginativeConjunctionBdd.Or(rootBdd);

                                    if (rootsForOriginativeConjunctionBdd != null && rootsForOriginativeConjunctionBdd.Roots.First().Children.Count == 0)
                                    {
                                        throw new Exception("An error occured while applying disjunction to bdds");
                                    }
                                }
                            }

                            if (rootsForOriginativeConjunctionBdd == null)
                            {
                                // no valid roots for current originative conjunction
                                continue;
                            }

                            // saving conditions for current originative conjunction
                            if (robustSensitezationConditionsForCurrentPath.ContainsKey(cube))
                            {
                                throw new Exception("Duplicate originative conjunction.");
                            }
                            robustSensitezationConditionsForCurrentPath.Add(cube, rootsForOriginativeConjunctionBdd);

                            // merging all conditions for all originative conjunctions
                            rootsBdd = rootsBdd == null
                                           ? rootsForOriginativeConjunctionBdd
                                           : rootsBdd.Or(rootsForOriginativeConjunctionBdd);

                        } // going to the next originative conjunction

                        // memorizing conditions for current path
                        robustSensitezationConditions.Add(robustSensitezationConditionsForCurrentPath);


                        // 
                        // 1. Calculating robust probability for random input pair
                        //

                        var pathObservability = 0.0;

                        if (rootsBdd != null)
                        {
                            var odnf = rootsBdd.Odnf();
                            if (odnf.Functions.Count != 1)
                            {
                                throw new Exception("Single function required.");
                            }

                            foreach (var cube in odnf.Functions[0].Domain1)
                            {
                                var cubeProbability = 1.0;
                                for (var i = 0; i < cube.Dimension; i++)
                                {
                                    if (cube[i] == BooleanValue.Undefined)
                                    {
                                        continue;
                                    }

                                    if (!inputProabilities.ContainsKey(inputMarks[i]))
                                    {
                                        throw new Exception("Undefined probability for variable!");
                                    }

                                    var varProbability = inputProabilities[inputMarks[i]];
                                    if (cube[i] == BooleanValue.True)
                                    {
                                        cubeProbability *= varProbability;
                                    }
                                    else
                                    {
                                        cubeProbability *= (1 - varProbability);
                                    }
                                }

                                pathObservability += cubeProbability;
                            }
                        }

                        // paths are statistically independent, hence, summorizing probabilities.
                        observability += pathObservability;


                        //
                        // 2. Calculating robust LoS(+1) probability
                        //

                        // retrieving all robust sensitezation conditions for current path


                        var losConditionsForCurrentPath = new List<Cube>();
                        foreach (DictionaryEntry conditionsForConjunction in robustSensitezationConditionsForCurrentPath)
                        {
                            var originativeConjunction = (Cube)conditionsForConjunction.Key;

                            // checking originative conjunction for incompatibility with LoS(+1) technique

                            // 1. Yj-1, Yj (j!=i) have opposite signs
                            var isIncompatible = false;
                            for (var j = 0; j < originativeConjunction.Dimension; j++)
                            {
                                if (j != currentStateVarIndex && originativeConjunction[j] != BooleanValue.Undefined &&
                                    stateVariablesOrderedIndices.Contains(j))
                                {
                                    // state var index
                                    var prevStateVarIndex =
                                        stateVariablesOrderedIndices[0] == j
                                            ? stateVariablesOrderedIndices[stateVariablesOrderedIndices.Count - 1]
                                            : stateVariablesOrderedIndices[stateVariablesOrderedIndices.IndexOf(j) - 1];

                                    if (originativeConjunction[prevStateVarIndex] != BooleanValue.Undefined &&
                                        originativeConjunction[j] != originativeConjunction[prevStateVarIndex])
                                    {
                                        isIncompatible = true;
                                        break;
                                    }
                                }
                            }

                            // 2. Yi-1, Yi+1 have same signs
                            if (originativeConjunction[previousToCurrentStateVarIndex] != BooleanValue.Undefined &&
                                originativeConjunction[previousToCurrentStateVarIndex] ==
                                originativeConjunction[nextToCurrentStateVarIndex])
                            {
                                // incompatible with LoS(+1) technique conjunction
                                isIncompatible = true;
                            }


                            #region SELF-TESTING

                            var losShift = originativeConjunction.Shift(1, stateVariablesOrderedIndices);
                            bool testPassed;

                            if (isIncompatible)
                            {
                                // incompatible test
                                testPassed = false;
                                for (var t = 0; t < stateVariablesOrderedIndices.Count; t++)
                                {
                                    if (stateVariablesOrderedIndices[t] != currentStateVarIndex)
                                    {
                                        if (losShift[stateVariablesOrderedIndices[t]] != BooleanValue.Undefined &&
                                            originativeConjunction[stateVariablesOrderedIndices[t]] !=
                                            BooleanValue.Undefined &&
                                            losShift[stateVariablesOrderedIndices[t]] !=
                                            originativeConjunction[stateVariablesOrderedIndices[t]])
                                        {
                                            testPassed = true;
                                            break;
                                        }
                                    }
                                    else
                                    {
                                        // t == i
                                        var nextStateVarIndex = (t + 1) >= stateVariablesOrderedIndices.Count
                                                                    ? 0
                                                                    : t + 1;
                                        if (originativeConjunction[stateVariablesOrderedIndices[nextStateVarIndex]] !=
                                            BooleanValue.Undefined &&
                                            losShift[stateVariablesOrderedIndices[t]] ==
                                            originativeConjunction[stateVariablesOrderedIndices[nextStateVarIndex]])
                                        {
                                            // current state variable has not changed it's value
                                            testPassed = true;
                                            break;
                                        }
                                    }
                                }
                            }
                            else
                            {
                                // compatible test
                                testPassed = true;
                                for (var t = 0; t < stateVariablesOrderedIndices.Count; t++)
                                {
                                    if (stateVariablesOrderedIndices[t] != currentStateVarIndex)
                                    {
                                        if (losShift[stateVariablesOrderedIndices[t]] != BooleanValue.Undefined &&
                                            originativeConjunction[stateVariablesOrderedIndices[t]] !=
                                            BooleanValue.Undefined &&
                                            losShift[stateVariablesOrderedIndices[t]] !=
                                            originativeConjunction[stateVariablesOrderedIndices[t]])
                                        {
                                            testPassed = false;
                                            break;
                                        }
                                    }
                                    else
                                    {
                                        // t == i
                                        var nextStateVarIndex = (t + 1) >= stateVariablesOrderedIndices.Count
                                                                    ? 0
                                                                    : t + 1;
                                        if (originativeConjunction[stateVariablesOrderedIndices[nextStateVarIndex]] !=
                                            BooleanValue.Undefined &&
                                            losShift[stateVariablesOrderedIndices[t]] ==
                                            originativeConjunction[stateVariablesOrderedIndices[nextStateVarIndex]])
                                        {
                                            // current state variable has not changed it's value
                                            testPassed = false;
                                            break;
                                        }
                                    }
                                }
                            }

                            if (!testPassed)
                            {
                                throw new Exception("Self testing failed. Invalid algorithm!");
                            }

                            #endregion


                            if (isIncompatible)
                            {
                                continue;
                            }

                            var currentPathConditionsForOneOriginativeConjunction = new List<Cube>();
                            var conditionsAsRobdd = (OrderedBdd)conditionsForConjunction.Value;
                            if (conditionsAsRobdd != null)
                            {
                                // extracting conditions from Robdd
                                var odnf = conditionsAsRobdd.Odnf();
                                if (odnf != null)
                                {
                                    if (odnf.Functions.Count != 1)
                                    {
                                        throw new Exception("Internal Error.");
                                    }

                                    currentPathConditionsForOneOriginativeConjunction = new List<Cube>(odnf.Functions[0].Domain1);
                                }
                            }

                            // reducing SoP by applying Blake algorithm (reduce SoP to SoPP)
                            var funcToReduct = new BooleanFunction
                                                   {
                                                       Domain1 =
                                                           new CubeSet(currentPathConditionsForOneOriginativeConjunction)
                                                   };
                            var reducedConditions = funcToReduct.Reduce().Domain1.ToList();

                            // appending additional LoS(+1) conditions to SoP and remove incompatible conjunctions
                            var incompatibleConjunctions = new HashSet<Cube>();
                            var additionalConjunctions = new List<Cube>();
                            foreach (var cube in reducedConditions)
                            {
                                var originalCube = new Cube(cube);

                                // appending LoS conditions for state vars stabilization
                                for (var j = 0; j < cube.Dimension; j++)
                                {
                                    if (!stateVariablesOrderedIndices.Contains(j))
                                    {
                                        // not state var
                                        continue;
                                    }

                                    if (cube[j] == BooleanValue.Undefined)
                                    {
                                        continue;
                                    }

                                    // prev state var index
                                    var prevStateVarIndex =
                                        stateVariablesOrderedIndices[0] == j
                                            ? stateVariablesOrderedIndices[stateVariablesOrderedIndices.Count - 1]
                                            : stateVariablesOrderedIndices[stateVariablesOrderedIndices.IndexOf(j) - 1];

                                    if (j != currentStateVarIndex && prevStateVarIndex != currentStateVarIndex)
                                    {
                                        // j != i && (j - 1) != i
                                        if (cube[prevStateVarIndex] == BooleanValue.Undefined)
                                        {
                                            cube[prevStateVarIndex] = cube[j];
                                        }
                                    }
                                }

                                // appending LoS conditions for changing value of current state var
                                Cube additionalCube = null;
                                if (cube[previousToCurrentStateVarIndex] != BooleanValue.Undefined &&
                                    cube[nextToCurrentStateVarIndex] != BooleanValue.Undefined)
                                {
                                    cube[currentStateVarIndex] = cube[nextToCurrentStateVarIndex];
                                }
                                else if (cube[nextToCurrentStateVarIndex] != BooleanValue.Undefined)
                                {
                                    cube[currentStateVarIndex] = cube[nextToCurrentStateVarIndex];
                                    cube[previousToCurrentStateVarIndex] = cube[nextToCurrentStateVarIndex] ==
                                                                           BooleanValue.True
                                                                               ? BooleanValue.False
                                                                               : BooleanValue.True;
                                }
                                else if (cube[previousToCurrentStateVarIndex] != BooleanValue.Undefined)
                                {
                                    cube[currentStateVarIndex] = cube[previousToCurrentStateVarIndex] ==
                                                                 BooleanValue.True
                                                                     ? BooleanValue.False
                                                                     : BooleanValue.True;
                                    cube[nextToCurrentStateVarIndex] = cube[currentStateVarIndex];
                                }
                                else
                                {
                                    // both absent (Yi-1 and Yi+1)
                                    cube[previousToCurrentStateVarIndex] = BooleanValue.False;
                                    cube[currentStateVarIndex] = BooleanValue.True;
                                    cube[nextToCurrentStateVarIndex] = BooleanValue.True;

                                    additionalCube = new Cube(cube);
                                    additionalCube[previousToCurrentStateVarIndex] = BooleanValue.True;
                                    additionalCube[currentStateVarIndex] = BooleanValue.False;
                                    additionalCube[nextToCurrentStateVarIndex] = BooleanValue.False;
                                }


                                // checking cube for incompatibility with LoS(+1) technique

                                // 1. Yj-1, Yj (j!=i) have opposite signs
                                isIncompatible = false;
                                var isIncompatibleAdditional = false; // for additional cube
                                for (var j = 0; j < cube.Dimension; j++)
                                {
                                    if (j != currentStateVarIndex && cube[j] != BooleanValue.Undefined &&
                                        stateVariablesOrderedIndices.Contains(j))
                                    {
                                        // next state var index
                                        var prevStateVarIndex =
                                            stateVariablesOrderedIndices[0] == j
                                                ? stateVariablesOrderedIndices[stateVariablesOrderedIndices.Count - 1]
                                                : stateVariablesOrderedIndices[
                                                    stateVariablesOrderedIndices.IndexOf(j) - 1];

                                        if (cube[prevStateVarIndex] != BooleanValue.Undefined &&
                                            cube[j] != cube[prevStateVarIndex])
                                        {
                                            isIncompatible = true;
                                        }

                                        // checking additional cube
                                        if (additionalCube != null &&
                                            additionalCube[prevStateVarIndex] != BooleanValue.Undefined &&
                                            additionalCube[j] != additionalCube[prevStateVarIndex])
                                        {
                                            isIncompatibleAdditional = true;
                                        }

                                        if (isIncompatible && isIncompatibleAdditional)
                                        {
                                            break;
                                        }
                                    }
                                }

                                // 2. Yi-1, Yi+1 have same signs
                                if (cube[previousToCurrentStateVarIndex] != BooleanValue.Undefined &&
                                    cube[previousToCurrentStateVarIndex] == cube[nextToCurrentStateVarIndex])
                                {
                                    // incompatible with LoS(+1) technique conjunction
                                    isIncompatible = true;
                                }

                                if (additionalCube != null &&
                                    additionalCube[previousToCurrentStateVarIndex] != BooleanValue.Undefined &&
                                    additionalCube[previousToCurrentStateVarIndex] ==
                                    additionalCube[nextToCurrentStateVarIndex])
                                {
                                    // incompatible with LoS(+1) technique conjunction
                                    isIncompatibleAdditional = true;
                                }


                                #region SELF-TESTING

                                losShift = cube.Shift(1, stateVariablesOrderedIndices);

                                if (isIncompatible)
                                {
                                    // incompatible test
                                    testPassed = false;
                                    for (var t = 0; t < stateVariablesOrderedIndices.Count; t++)
                                    {
                                        if (stateVariablesOrderedIndices[t] != currentStateVarIndex)
                                        {
                                            if (losShift[stateVariablesOrderedIndices[t]] != BooleanValue.Undefined &&
                                                cube[stateVariablesOrderedIndices[t]] != BooleanValue.Undefined &&
                                                losShift[stateVariablesOrderedIndices[t]] !=
                                                cube[stateVariablesOrderedIndices[t]])
                                            {
                                                testPassed = true;
                                                break;
                                            }
                                        }
                                        else
                                        {
                                            // t == i
                                            var nextStateVarIndex = (t + 1) >= stateVariablesOrderedIndices.Count
                                                                        ? 0
                                                                        : t + 1;
                                            if (cube[stateVariablesOrderedIndices[nextStateVarIndex]] !=
                                                BooleanValue.Undefined &&
                                                losShift[stateVariablesOrderedIndices[t]] ==
                                                cube[stateVariablesOrderedIndices[nextStateVarIndex]])
                                            {
                                                // current state variable has not changed it's value
                                                testPassed = true;
                                                break;
                                            }
                                        }
                                    }
                                }
                                else
                                {
                                    // compatible test
                                    for (var t = 0; t < stateVariablesOrderedIndices.Count; t++)
                                    {
                                        if (stateVariablesOrderedIndices[t] != currentStateVarIndex)
                                        {
                                            if (originalCube[stateVariablesOrderedIndices[t]] != BooleanValue.Undefined &&
                                                losShift[stateVariablesOrderedIndices[t]] !=
                                                originalCube[stateVariablesOrderedIndices[t]])
                                            {
                                                testPassed = false;
                                                break;
                                            }
                                        }
                                        else
                                        {
                                            // t == i
                                            if (originalCube[stateVariablesOrderedIndices[t]] != BooleanValue.Undefined &&
                                                losShift[stateVariablesOrderedIndices[t]] ==
                                                originalCube[stateVariablesOrderedIndices[t]])
                                            {
                                                // current state variable has changed it's value
                                                testPassed = false;
                                                break;
                                            }
                                        }
                                    }
                                }

                                if (!testPassed)
                                {
                                    throw new Exception("Self testing failed. Invalid algorithm!");
                                }

                                #endregion


                                if (isIncompatible)
                                {
                                    // incompatible cube
                                    incompatibleConjunctions.Add(cube);
                                }

                                if (additionalCube != null && !isIncompatibleAdditional)
                                {
                                    // compatible additional cube
                                    additionalConjunctions.Add(additionalCube);
                                }


                            } // next cube


                            // removing incompatible conjunctions
                            reducedConditions =
                                reducedConditions.Where(c => !incompatibleConjunctions.Contains(c)).ToList();

                            // adding additional conjunctions
                            reducedConditions.AddRange(additionalConjunctions);

                            // appending conditions to main set
                            losConditionsForCurrentPath.AddRange(reducedConditions);

                        } // next originative conjunction



                        // LoS conditions appended, orthogonalizing SoP
                        rootsBdd = null;
                        foreach (var cube in losConditionsForCurrentPath)
                        {
                            // building bdd representing condition
                            var rootBdd = OrderedBdd.BuildFromCube(cube, inputMarks);

                            // orthogonalizing
                            rootsBdd = rootsBdd == null ? rootBdd : rootsBdd.Or(rootBdd);

                            if (rootsBdd != null && rootsBdd.Roots.First().Children.Count == 0)
                            {
                                throw new Exception("An error occured while applying disjunction to bdds");
                            }
                        }


                        // calculating LoS probabilities

                        var pathLosObservability = 0.0;

                        if (rootsBdd != null)
                        {
                            var odnf = rootsBdd.Odnf();
                            if (odnf.Functions.Count != 1)
                            {
                                throw new Exception("Single function required.");
                            }

                            foreach (var cube in odnf.Functions[0].Domain1)
                            {
                                var cubeProbability = 1.0;
                                for (var i = 0; i < cube.Dimension; i++)
                                {
                                    if (cube[i] == BooleanValue.Undefined)
                                    {
                                        continue;
                                    }

                                    if (!inputProabilities.ContainsKey(inputMarks[i]))
                                    {
                                        throw new Exception("Undefined probability for variable!");
                                    }

                                    var varProbability = inputProabilities[inputMarks[i]];
                                    if (cube[i] == BooleanValue.True)
                                    {
                                        cubeProbability *= varProbability;
                                    }
                                    else
                                    {
                                        cubeProbability *= (1 - varProbability);
                                    }
                                }

                                pathLosObservability += cubeProbability;
                            }
                        }


                        // paths are statistically independent, hence, summorizing probabilities.
                        losObservability += pathLosObservability;

                    } // next path
                    #endregion

                    resultsFroDifferentTreeTops.Add(new FlipFlopStats
                                   {
                                       InputMarks = inputMarks,
                                       OutputMarks = outputMarks,
                                       InputMark = stateVariableMark,
                                       OutputMark = outputMark,
                                       RobustObservability = observability,
                                       RobustLosObservability = losObservability,
                                       RobustSensitezationConditions = robustSensitezationConditions
                                   });

                } // next tree top (circuit output)

                result.Add(resultsFroDifferentTreeTops);

            } // next state variable

            return result;
        }
    }
}
